T:Type, l:IdLnk, tg:Id, L:MsgA List. (ML. T  M.din(l,tg))  T  (L).din(l,tg) 

latex

Definitions	SQType(T), {T}, False, P  Q, KindDeq, f(x)?z, Unit, x  dom(f), rcv(l,tg), f  g, a:A fp B(a), Knd, f(x), , b, A, b, Valtype(da;k), MsgAForm, P  Q, P & Q, M1  M2, P  Q, xL. P(x), x. t(x), Prop, , M.din(l,tg), mk-ma, Top, IdLnk, Id, x:A. B(x), t  T, MsgA, (L)
Lemmas	msga wf, Id wf, IdLnk wf, top wf, ma-din wf, subtype rel wf, l all wf, l all cons, msg-form wf, ma-join-list wf, msg-form-join-list, assert wf, not wf, bnot wf, bool wf, fpf-trivial-subtype-top, fpf-join wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, fpf-join-ap-sq, fpf-join-dom, bool sq, bool cases